In the hardware design industry, having a design error can be disastrous. In the Intel Pentium P5 chip, a floating point division bug caused Intel to lose up to $475 million in 1995. More recently in 2007, AMD encountered a virtualization bug in its Phenom line of CPUs requiring them to revise the silicon, a costly procedure. Unlike software bugs, hardware bugs cannot always be fixed with a simple patch. These bugs cost hardware manufacturers millions of dollars and precious time in a quickly moving industry.
Assertions or invariants provide a mechanism to express desirable properties that should be true in the system. Assertions are used for validating hardware designs at different stages through their life-cycle, such as pre-silicon formal verification, dynamic validation, runtime monitoring and emulation. Assertions are also synthesized into hardware for post-silicon debug and validation and in-field diagnosis.
Among all the solutions for ensuring robustness of hardware systems, assertion based verification has emerged as the most popular candidate solution for “pre-silicon” design functionality checking. Assertions are used for static (formal) verification as well as dynamic verification of the register transfer level (RTL) design in the pre-silicon phase.
Assertion generation is an entirely manual effort in the hardware system design cycle. Placing too many assertions can result in an unreasonable performance overhead. Placing too few assertions, on the other hand, results in insufficient coverage of behavior. The trade-off point for crafting minimal, but effective (high coverage) assertions takes multiple iterations and man-months to achieve. Another challenge with assertion generation is due to the modular nature of system development. A module developer would write local assertions that pertain to his/her module. Maintaining consistency of inter-modular global assertions as the system evolves in this fragmented framework is very tedious. In sequential hardware, temporal properties that cut across time cycles are usually the source of subtle, but serious bugs. It is difficult for the human mind to express and reason with temporal relations, making temporal assertion generation very challenging.